Define flatness of a sheaf of modules `F` on a scheme `X` over a base `S`
via a morphism `f : X ⟶ S`: `Scheme.Modules.FlatAt f F x` is the pointwise
condition that the stalk `F_x` is flat over `𝒪_{S, f(x)}` (acting through
`f.stalkMap x`), and `Scheme.Modules.Flat f F` asserts `∀ x, FlatAt f F x`.

Main results:
* `Scheme.Modules.flat_tilde_iff` / `flat_tilde_iff_of_algebra`: affine
  criteria identifying flatness of `M^~` with flatness of `M`.
* `Scheme.Modules.Flat.comp`: transitivity along a flat base.
* `Scheme.Modules.flat_comp_isOpenImmersion_iff`: locality on the base.
* `Scheme.Modules.flat_iff_forall_openCover`: locality on the source.

Supporting `RingTheory` lemmas:
* `Module.compHom_smul` (`Algebra/Module/RingHom`)
* `Module.Flat.tensor_tower` (`RingTheory/Flat/Stability`)
* `Module.flat_iff_forall_localizedModule_prime`,
  `Module.Flat.localizedModule_base`,
  `Module.flat_iff_forall_localizedModule_prime_of_algebra`
  (`RingTheory/Flat/Localization`)
* `Module.Flat.trans_compHom`, `Module.Flat.compHom_bijective_iff`
  (`RingTheory/RingHom/Flat`)

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…tilde_iff_of_algebra

Address PR review: derive the affine-case `flat_tilde_iff` (identity morphism)
as the special case `f = 𝟙 R` of the general `flat_tilde_iff_of_algebra`,
removing the now-redundant identity-specific helpers `Tilde.compHom_stalkMap_id_eq`
and `Tilde.stalk_flat_iff`.

Note: could not be compiled locally; the branch requires the lean toolchain
v4.32.0-rc1 which is not provisioned in this environment.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>